import assert from 'node:assert/strict'
import {type Formula, stringify} from '../src/formula.js'
import {Parser} from '../src/parser.js'

const article = `

environ
relations <, isPrime, |_|, cool;
operations + precedence 64, ' precedence 5, ^ precedence 100;
operations * precedence 60, 0;
brackets [: :], (* *);

environ
type Real;
type Nat -> Real;
type Dummy;

pred cool;
pred Real < Real;
pred |_| Nat;
pred |_| Real, Real, Nat;
pred isPrime Nat;

func 0 -> Nat;
func Nat + Nat -> Nat;
func Nat, Nat + Nat, Nat -> Nat;
func Nat, Nat * Nat, Nat -> Nat;
func Nat * Nat -> Nat;
func ^Nat -> Nat;
func Nat' -> Nat;
func Nat, Nat' -> Nat;
func [: Nat,Real :] -> Nat;
func [: Nat,Nat,Nat :] -> Nat;

reserve x,y,z for Real, m,n for Nat;

1: true implies true;
1: true implies false;
1: not false;
1: (false iff true) iff false;
1: (false iff true) implies false;
1: true & not (false iff true) implies false;
9: true & not true implies false;
1: true & (true implies true);
1: true & false or (false iff true);
1: true & for x, y, z holds true;
1: true & for x, y be Nat ex z st true;
1: true or  ex x st true iff true;
1: for n,y holds n < y;
1: ex n,m st (cool implies for n st cool holds not |_| [:n,m:]);
1: ex n,m st not |_| [:[:n,m:],m:]''' + (n *m,n  )'   ''+ m'' '*n ' '';
1: ex n,m st |_| n + (^[:n * m, n:]' + m' * n');


`

function runParser(article: string) {
    const parser = new Parser(article)
    const errors: string[] = []
    parser.setErrorLogger(error => errors.push(error))
    parser.parseArticle()
    return errors
}

it('must verify default article OK', () => {
    assert.equal(runParser(article).length, 0)
})

it('must verify &-e OK', () => {
    const text = `

        ${article}

        1: (cool & cool & true) & (cool & true);
        text
        2: cool by 1;

    `

    assert.equal(runParser(text).length, 0)
})

it('must fail incorrect &-e', () => {
    const text = `

        ${article}

        1: (cool & cool & true) & (cool & true);
        text
        false by 1;

    `

    assert.equal(runParser(text).length, 1)
})

it('must fail incorrect or-e', () => {
    const text = `

        environ
        relations cool, foo;
        pred cool;
        pred foo;

        1: true or (cool or false or not foo) or true;
        2: not foo implies false;
        3: cool implies false;
        text
        false by 1,2,3;

    `

    assert.equal(runParser(text).length, 1)
})

it('must verify or-e OK', () => {
    const text = `

        environ
        relations cool, foo;
        pred cool;
        pred foo;

        1: true or (cool or cool);
        2: true implies false;
        3: cool implies false;
        text
        false by 1,2,3;

    `

    assert.equal(runParser(text).length, 0)
})

it('must verify implies-e OK', () => {
    const text = `

        environ
        relations foo, bar;
        pred foo;
        pred bar;

        1: foo implies bar;
        2: foo;
        text
        bar by 1,2;

    `

    assert.equal(runParser(text).length, 0)
})

it('must verify iterative implies-e OK', () => {
    const text = `

        environ
        relations foo, bar;
        pred foo;
        pred bar;

        1: foo implies (bar implies false);
        2: foo;
        3: bar;
        text
        false by 1,2,3;

    `

    assert.equal(runParser(text).length, 0)
})

it('must verify iterative2 implies-e OK', () => {
    const text = `

        environ
        relations foo, bar;
        pred foo;
        pred bar;

        1: foo implies bar;
        2: bar implies false;
        3: foo;
        text
        false by 1,2,3;

    `

    assert.equal(runParser(text).length, 0)
})

it('must fail incorrect implies-e', () => {
    const text = `

        environ
        relations foo, bar, baz;
        pred foo;
        pred bar;
        pred baz;

        1: foo implies baz;
        2: bar implies baz;
        3: foo;
        text
        foo by 1;
        foo by 1,2;
        foo by 1,2,4;
        bar by 1;
        bar by 1,2;
        bar by 1,2,3;
        baz by 1,2;
        baz by 2,3;

    `

    assert.equal(runParser(text).length, 8)
})

it('must accept proof without "thus true"', () => {
    const text = `

        text
        true proof qed;

        false implies true
        proof
            assume false;
        qed;
    `

    assert.equal(runParser(text).length, 0)
})

it('must fail invalid proof', () => {
    const text = `

        text
        false proof qed;

        false implies false
        proof
            assume false;
        qed;
    `

    assert.equal(runParser(text).length, 2)
})

it('must verify assume and thus OK', () => {
    const text = `

        ${article}

        text
        cool implies (cool & cool & true) & (cool & true)
        proof
            assume 1: cool;
            2: true;
            thus cool & cool & true by 1,2;
            thus cool & true by 1,2;
        qed;

    `

    assert.equal(runParser(text).length, 0)
})

it('must verify chained assume and thus OK', () => {
    const text = `

        ${article}

        text
        cool implies (cool & cool & true) implies (cool & true)
        proof
            assume 1: cool and 2: cool & cool & true;
            3: true;
            thus cool & true by 1,3;
        qed;

    `

    assert.equal(runParser(text).length, 0)
})

it('must accept chained assume', () => {
    const text = `

        ${article}

        text
        cool implies (cool & cool & true) implies (cool & true)
        proof
            assume 1: cool and cool and cool;
            assume 3: true;
            thus cool & true by 1,3;
        qed;

    `

    assert.equal(runParser(text).length, 0)
})

it('must verify partial thus OK', () => {
    const text = `

        ${article}

        text
        cool implies (cool & true & cool & true)
        proof
            assume 1: cool;
            thus cool by 1;
            thus 2: true;
            thus cool & true by 1,2;
        qed;

    `

    assert.equal(runParser(text).length, 0)
})

it('must verify inner proof OK', () => {
    const text = `

        ${article}

        text
        cool implies (cool & true & cool & true)
        proof
            assume 1: cool;
            thus cool
            proof
                thus cool by 1;
            qed;
            thus 2: true;
            thus cool & true by 1,2;
        qed;

    `

    assert.equal(runParser(text).length, 0)
})

it('must fail label accessing from inner proof', () => {
    const text = `

        ${article}

        text
        cool implies (cool & cool & true)
        proof
            assume 1: cool;
            thus cool
            proof
                thus cool by 1;
                3: true;
            qed;
            thus cool & true by 1,3;
        qed;

    `

    assert.equal(runParser(text).length, 2)
})

it('must fail incorrect assume and thus', () => {
    const text = `

        ${article}

        text
        cool implies (cool & cool & true) & (cool & true)
        proof
            assume true and 1: cool and false;
            thus 2: true;
            thus cool & cool & true by 1,2;
            thus cool & true by 1,2;
        qed;

    `

    assert.equal(runParser(text).length, 3)
})

it('must verify let OK', () => {
    const text = `

        ${article}

        text
        for n holds n < n or true
        proof
            let n;
            1: true;
            thus n < n or true by 1;
        qed;

    `

    assert.equal(runParser(text).length, 0)
})

it('must verify let such that OK', () => {
    const text = `

        ${article}

        text
        for n,m st false holds n < m
        proof
            let m,n such that 1: false;
            thus m < n by 1;
        qed;

    `

    assert.equal(runParser(text).length, 0)
})

it('must fail incorrect let', () => {
    const text = `

        ${article}

        text
        for x,y st false holds x < y
        proof
            let x,y being Nat such that 1: false;
            thus thesis by 1;
        qed;

    `

    assert.equal(runParser(text).length, 2)
})

it('must verify proof with thesis OK', () => {
    const text = `

        ${article}

        text
        cool implies (cool & true & cool & true)
        proof
            assume 1: cool;
            thus thesis
            proof
                2: true;
                thus thesis by 1,2;
            qed;
            thus 2: true;
            thus thesis by 1,2;
        qed;

    `

    assert.equal(runParser(text).length, 0)
})

it('must support "hence"', () => {
    const text = `

        ${article}

        text
        cool implies true & true & true
        proof
            assume 1: cool;
            2: true;
            3: true & true by 2;
            hence thesis by 2;
        qed;

    `

    assert.equal(runParser(text).length, 0)
})

it('must fail invalid "hence"', () => {
    const text = `

        ${article}

        text
        true
        proof
            hence thesis;
        qed;

    `

    assert.equal(runParser(text).length, 1)
})

it('must support "then"', () => {
    const text = `

        ${article}

        text
        cool implies true & true & true
        proof
            assume 1: cool;
            2: true;
            then true & true;
            then 3: true & true;
            hence thesis by 2;
        qed;

    `

    assert.equal(runParser(text).length, 0)
})

it('must fail invalid "then"', () => {
    const text = `

        ${article}

        text
        begin
            then true;
            consider x;
            then true;
            consider x such that true;
            then true;
        end;

    `

    const errors = runParser(text)

    assert.equal(errors.length, 2)
    assert.equal(errors.every(error => error == 'invalid "then" usage'), true)
})

it('must fail invalid "hence"', () => {
    const text = `

        ${article}

        text
        begin
            hence true;
            consider x;
            hence true;
        end;

    `

    const errors = runParser(text)

    assert.equal(errors.length, 2)
    assert.equal(errors.every(error => error == 'invalid "hence" usage'), true)
})

it('must fail invalid inference', () => {
    const text = `

        ${article}

        text
        cool implies true
        proof
            cool;
            thus thesis;
        qed;

    `

    assert.equal(runParser(text).length, 2)
})

it('must support "given"', () => {
    const text = `

        ${article}

        text
        (ex n st n < n) implies true
        proof
            given n;
            assume n < n;
            thus thesis;
        qed;

    `

    assert.equal(runParser(text).length, 0)
})

it('must support "given" with "such that"', () => {
    const text = `

        ${article}

        text
        (ex n st n < n & false) implies false
        proof
            given n such that n < n & false;
            hence thesis;
        qed;

    `

    assert.equal(runParser(text).length, 0)
})

it('must fail invalid "given"', () => {
    const text = `

        ${article}

        text
        (ex x st true) implies true
        proof
            given n such that true;
            thus thesis;
        qed;

    `

    const errors = runParser(text)

    assert.equal(errors[0], 'existential assumption disagrees with thesis')
    assert.equal(errors.length, 3)
})

it('must support contructor function', () => {
    const text = `

        environ
        operations o, s;
        type Nat;

        constructor o -> Nat;
        constructor s Nat -> Nat;

    `

    assert.equal(runParser(text).length, 0)
})

it('must fail mismatched operation position', () => {
    const text = `

        ${article}

        1: for n, m holds (n, n, n, m) + = m;
        1: for n, m holds (n, n, n) * m = m;
        1: ex n, m st n + (m, m, m) = m;

    `

    assert.equal(runParser(text).length, 6)
})

it('must accept matched operation position', () => {
    const text = `

        ${article}

        1: ex n, m st (n, n) + (m, m) = m;
        1: for n, m holds (n, n) * (m, m) = m;

    `

    assert.equal(runParser(text).length, 0)
})

it('must accept "consider"', () => {
    const text = `

        ${article}

        text

        true
        proof
            consider n;
            consider n;
            thus thesis;
        qed;

    `

    const errors = runParser(text)

    assert.equal(errors.length, 0)
})

it('must accept "consider" with "such that"', () => {
    const text = `

        ${article}

        1: ex n,m st n < n & true & cool;

        text

        true
        proof
            consider n,m such that n < n & true & cool by 1;
            consider n,m such that n < n and true & cool by 1;
            consider n,m such that n < n and true and cool by 1;
            consider n such that ex m st n < n & true & cool by 1;
            then consider m such that n < n and true & cool;
            thus thesis;
        qed;

    `

    const errors = runParser(text)

    assert.equal(errors.length, 0)
})

it('must accept "consider" with "such that true"', () => {
    const text = `

        ${article}

        text

        true
        proof
            consider n such that true;
            consider n such that true;
            thus thesis;
        qed;

    `

    const errors = runParser(text)

    assert.equal(errors.length, 0)
})

it('must fail invalid "consider"', () => {
    const text = `

        ${article}

        1: ex x,y st x < y;

        text

        true
        proof
            consider x,y such that x < y;
            consider x,y such that cool by 1;
            consider n,y such that n < y by 1;
            consider x such that x < y by 1;
            thus thesis;
        qed;

    `

    const errors = runParser(text)

    assert.equal(errors.length, 4)
    assert.equal(errors.every(error => error == 'choice not accepted'), true)
})

it('must accept "given" followed by "thus implies"', () => {
    const text = `

        ${article}

        text

        for x st false holds (ex y,z st y < z) implies true
        proof
            let x such that false;
            given y;
            given z;
            thus y < z implies true
            proof
                assume y < z;
                thus true;
            qed;
        qed;

    `

    const errors = runParser(text)

    assert.equal(errors.length, 0)
})

it('must accept "given" followed by "thus"', () => {
    const text = `

        ${article}

        text

        begin
            begin
                given x;
                thus true;
            end;
            then (ex x st true) implies true;
        end;

    `

    const errors = runParser(text)

    assert.equal(errors.length, 0)
})

it('must accept "begin"', () => {
    const text = `

        ${article}

        text

        begin
            begin
                let x such that false;
                given y;
                given z;
                assume y < z;
                hence true;
            end;
            then for x st false holds (ex y,z st y < z) implies true;
        end;

    `

    const errors = runParser(text)

    assert.equal(errors.length, 0)
})

it('must fail "thesis" in "begin"', () => {
    const text = `

        ${article}

        text

        begin
            thus thesis;
        end;

    `

    const errors = runParser(text)

    assert.equal(errors.length, 1)
    assert.equal(errors[0], '"thesis" not allowed here')
})

it('must accept "take"', () => {
    const text = `

        ${article}

        text

        ex x,y st ((ex m,n st m < n) implies x < y or true)
        proof
            begin
                take x,y;
                given m,n;
                assume m < n;
                true;
                hence x < y or true;
            end;
            hence thesis;
        qed;

    `

    const errors = runParser(text)

    assert.equal(errors.length, 0)
})

it('must fail invalid proof with "take"', () => {
    const text = `

        ${article}

        text

        ex x,y st x < y or true
        proof
            begin
                take x,y;
                true;
                hence x < x or true;
            end;
            hence thesis;
        qed;

    `

    const errors = runParser(text)

    assert.equal(errors.length, 1)
})

it('must accept indirect proof', () => {
    const text = `

        ${article}

        text

        true
        proof
            assume 1: not true;
            true;
            hence false by 1;
        qed;

        true
        proof
            assume 1: not true;
            assume 2: not false;
            true;
            then true or false;
            hence false by 1,2;
        qed;

    `

    const errors = runParser(text)

    assert.equal(errors.length, 0)
})

it('must accept proof with "="', () => {
    const text = `

        ${article}

        text

        for x,y st x=((y)) holds (((x))=y)
        proof
            let x,y such that ((x))=y;
            hence x=(((y)));
        qed;

    `

    const errors = runParser(text)

    assert.equal(errors.length, 0)
})

it('must fail "=" with unrelated typed terms', () => {
    const text = `

        environ
        type Nat;
        type Set;

        1: for x be Nat,y be Set holds x=y;

    `

    const errors = runParser(text)

    assert.equal(errors.length, 1)
    assert.equal(errors[0], '"Nat" and "Set" types not related')
})

it('must accept "n = n"', () => {
    const text = `

        environ
        type Nat;

        text
        begin
            let n be Nat;
            thus n = n;
        end;

    `

    const errors = runParser(text)

    assert.equal(errors.length, 0)
})

it('must fail invalid "n = m"', () => {
    const text = `

        environ
        type Nat;

        text
        begin
            let n be Nat, m be Nat;
            thus n = m;
        end;

    `

    const errors = runParser(text)

    assert.equal(errors.length, 1)
})

function parseFormula(formula: string) {
    const parser = new Parser(`
        ${article}
        100: ${formula};
    `)
    const errors: string[] = []
    parser.setErrorLogger(error => errors.push(error))
    parser.parseArticle()
    return [parser.verifier.formulae[100] as Formula, errors] as const
}

it('must stringify simple formulas', () => {
    const formulas = [
        'true or false',
        'cool & cool',
        '(cool or cool) or false',
        'not cool implies cool',
        'not (not cool iff not cool)',
    ]

    for (const formula of formulas)
        assert.equal(formula, stringify(parseFormula(formula)[0]))
})

it('must stringify formulas with terms', () => {
    const formulas = [
        '0 is Nat',
        '0 < 0',
        'ex n be Nat st 0 = n \' + n',
        // '0 < 0 + 0',  TODO fix parsing zero-arity functions (precedence problem?)
    ]

    for (const formula of formulas) {
        const [roundbackFormula, errors] = parseFormula(formula)
        assert.deepEqual(errors, [])
        errors.length || assert.equal(formula, stringify(roundbackFormula))
    }
})
